Nuprl Lemma : int_add_grp_wf
13,42
postcript
pdf
<
+>
AbGrp{1}
latex
Up
groups
1
Definitions of Statement
|
g
|
,
*
,
Mon
,
Group{i}
,
AbGrp
,
<
+>
Definitions
<
+>
,
AbGrp
,
t
T
,
P
&
Q
,
x
.
t
(
x
)
,
P
Q
,
,
P
Q
,
x
f
y
,
P
Q
,
x
:
A
.
B
(
x
)
,
IsEqFun(
T
;
eq
)
,
Assoc(
T
;
op
)
,
Ident(
T
;
op
;
id
)
,
Inverse(
T
;
op
;
id
;
inv
)
,
t
.2
,
t
.1
,
*
,
|
g
|
,
Comm(
T
;
op
)
,
Mon
,
Group{i}
,
x
(
s
)
Lemmas
grp
op
wf
,
grp
car
wf
,
comm
wf
,
le
int
wf
,
eq
int
wf
,
mk
grp
,
assert
of
eq
int
,
iff
functionality
wrt
iff
,
assert
wf
,
iff
wf
,
all
functionality
wrt
iff
origin